refactor(CategoryTheory/Generator): use ObjectProperty instead of Set #30269
Conversation
PR summary 0d837987e5
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Comma.StructuredArrow.Small | 483 | 459 | -24 (-4.97%) |
| Mathlib.CategoryTheory.Generator.Basic | 758 | 759 | +1 (+0.13%) |
| Mathlib.CategoryTheory.Generator.Presheaf | 759 | 760 | +1 (+0.13%) |
| Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems | 773 | 772 | -1 (-0.13%) |
| Mathlib.CategoryTheory.Generator.HomologicalComplex | 777 | 778 | +1 (+0.13%) |
| Mathlib.CategoryTheory.Generator.Sheaf | 791 | 792 | +1 (+0.13%) |
| Mathlib.CategoryTheory.Generator.Preadditive | 849 | 850 | +1 (+0.12%) |
| Mathlib.CategoryTheory.Generator.Indization | 970 | 971 | +1 (+0.10%) |
| Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives | 1147 | 1148 | +1 (+0.09%) |
| Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator | 1352 | 1353 | +1 (+0.07%) |
| Mathlib.Algebra.Category.ModuleCat.AB | 1364 | 1365 | +1 (+0.07%) |
| Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu | 1465 | 1466 | +1 (+0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.CategoryTheory.Comma.StructuredArrow.Small |
-24 |
Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems |
-1 |
22 filesMathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf Mathlib.Condensed.AB Mathlib.Condensed.Light.AB |
1 |
Declarations diff
+ CostructuredArrow.isSeparating_proj_preimage
+ IsCodetecting.of_le
+ IsCoseparating.of_equivalence
+ IsCoseparating.of_le
+ IsDetecting.of_le
+ IsSeparating.of_equivalence
+ IsSeparating.of_le
+ ObjectProperty.IsSeparating.isSeparator_coproduct
+ StructuredArrow.isCoseparating_proj_preimage
+ instance : ObjectProperty.Small.{u} (freeYoneda R) := by
+ isCodetecting_bot_of_isGroupoid
+ isCoseparating_bot_of_isThin
+ isCoseparating_inverseImage_proj
+ isCoseparator_iff_of_isLimit_fan
+ isCoseparator_of_isLimit_fan
+ isDetecting_bot_of_isGroupoid
+ isGroupoid_of_isCodetecting_bot
+ isGroupoid_of_isDetecting_bot
+ isSeparating_bot_of_isThin
+ isSeparating_inverseImage_proj
+ isSeparator_iff_of_isColimit_cofan
+ isThin_of_isCoseparating_bot
+ isThin_of_isSeparating_bot
++ small_inverseImage_proj_of_locallySmall
++- IsCodetecting.isCoseparating
++- IsCodetecting.isIso_iff_of_epi
++- IsCoseparating.isCodetecting
++- IsDetecting.isIso_iff_of_mono
++- IsDetecting.isSeparating
++- IsSeparating.isDetecting
++- isCodetecting_iff_isCoseparating
++- isCodetecting_unop_iff
++- isCoseparating_unop_iff
++- isDetecting_unop_iff
++- isSeparating_unop_iff
++-- small_proj_preimage_of_locallySmall
+-+ IsCodetecting
+-+ IsCoseparating
+-+ IsDetecting
+-+ IsSeparating
+-+ isCodetecting_op_iff
+-+ isCoseparating_iff_mono
+-+ isCoseparating_op_iff
+-+ isDetecting_iff_isSeparating
+-+ isDetecting_op_iff
+-+ isSeparating_iff_epi
+-+ isSeparating_op_iff
- instance : Small.{u} (freeYoneda R) := by
- isCoseparating_proj_preimage
- isSeparating_proj_preimage
-+--++ isSeparating
--++ isSeparator
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
github-actions
bot
added
the
large-import
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
…tes' into refactor-isseparating
This PR adds the prerequisites for the refactor PR #30269, mostly the addition of `ObjectProperty.op` and constructors for `ObjectProperty` given by families of objects.
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
github-actions
bot
removed
the
large-import
…er-community#30294) This PR adds the prerequisites for the refactor PR leanprover-community#30269, mostly the addition of `ObjectProperty.op` and constructors for `ObjectProperty` given by families of objects.
jcommelin
changed the title
|
|
||
| variable (P : ObjectProperty C) | ||
|
|
||
| /-- We say that `P : ObjectProperty C` is a separating set if the functors `C(G, -)` |
There was a problem hiding this comment.
Very very minor nitpick, but is it still worth saying "separating set" in docstrings when they are now object properties (which are, admittedly, just an alias for sets)?
| /-- We say that `P : ObjectProperty C` is a separating set if the functors `C(G, -)` | |
| /-- We say that `P : ObjectProperty C` is separating if the functors `C(G, -)` |
Same question for the docs in the few definitions below.
| · simpa [β, b] using huv =≫ Pi.π (b A) ⟨⟨G, hG⟩, f⟩ | ||
| · rw [← cancel_mono (Pi.lift (Sigma.snd (β := β Y)))] | ||
| ext ⟨⟨_, hG⟩, _⟩ | ||
| simp |
There was a problem hiding this comment.
| simp |
robin-carlier
added
the
awaiting-author
3 participants
In certain applications (see #30247), it becomes unpractical to have certains notions like
IsSeparatingdefined forSet C, while the API for the relatively newObjectPropertyis expanding. In this PR, we move the definition ofIsSeparatingto theObjectPropertynamespace.